perm filename NEU[1,JRA] blob sn#005888 filedate 1972-10-25 generic text, type T, neo UTF8
00050	 VAR: x,y,z,u,v,X,Y,Z,U,V;INF_OP:⊗;
00075	INF_PRED: =; EQUALITY: =;
00087	PRE_OP: 1;
00100	G1: x⊗x = y⊗y;
00200	G2: x⊗(y⊗y) = x;
00300	df: x⊗x=1;
00600	G3:(x⊗z)⊗(y⊗z) = x⊗y;
00650	THEOREM: x⊗(1⊗y) = z ≡ z⊗y =x;
00700	;